A significant objective of program analysis and verification is to determine that a given software code performs its intended functions correctly, to ensure that it performs no unintended functions, and to provide information about its quality and reliability. Flaws in the overall design of software generally lead to bugs and problems in the implementation of the software. Several techniques currently exist for verifying software design and requirements. Two well known techniques include symbolic model checking and abstract interpretation.
Qualitatively, symbolic model checking involves the definition of system requirements or design (called models) and a property (called the specification) that the final system is expected to satisfy. The model checking construct indicates whether a specified model satisfies given specifications, and if it does not, indicates why the model does not satisfy the specification. Abstract interpretation consists of providing several semantics linked by relations of abstraction. A semantic is a mathematical characterization of the possible behaviors of the program.
At a fundamental level, program analysis and verification techniques such as model checking and abstract interpretation make use of existential quantifier elimination. An existential quantifier is a logical symbol “∃” that allows potential simplification of a formula by eliminating some set of variables V from the formula.
Given a quantifier-free formula φ and a set of variables V, existentially quantifying away V involves computing a quantifier-free formula that is logically equivalent to ∃V: φ. This operation is useful in practice to eliminate variables that are no longer necessary from a formula. For instance, the image computation in symbolic model checking involves computing the quantifier-free formula equivalent to ∃V: R(V)T(V,V′). Here, R(V) represents the current set of reachable states and T (V,V′) represents the transition relation between the current values of the state variables V and their new values V′. Existential Quantifier Elimination is also useful in computing the strongest postcondition across an assignment node in abstract interpretation, wherein the invariant I′ after an assignment node x:=e is obtained from the invariant I before the assignment node by performing the following computation: ∃x′I[x′/x]x=e[x′/x].
Existential quantifier elimination can be performed, albeit with exponential complexity, for propositional formulas. However, this operation is not defined for formulas containing interpreted symbols from certain theories. For example, consider the formula F(x)=0 in the theory of uninterpreted functions. There is no quantifier-free formula that is equivalent to ∃x: F(x)=0 as it is not possible to state that 0 is in the range of function F without using quantifiers. Similarly, the theory of lists and the theory of arrays do not admit existential quantifier elimination. This limits the application of techniques like symbolic model checking to systems described by formulas in these theories.
There exist techniques to approximate existential quantifier elimination when it does not exist (as in the above-cited instances of uninterpreted formulas, the theory of lists and the theory of arrays). Such techniques guarantee soundness in performing program analysis and verification techniques. That is, when these approximations indicate that a program verifies true, that is an accurate result. These approximations are disclosed for example in the publications T. Ball and S. K. Rajamani, “The SLAM project: Debugging system software via static analysis,” In 29th Annual Symposium on POPL, pages 1-3, 2002, and S. Chaki et al., “Modular verification of software components in C,” Transactions on Software Engg., 30(6):388-402, 2004.
However, conventional approximation theories are not precise in performing program analysis and verification techniques where existential quantifier elimination is not possible. That is, they can on occasion give a false indication that a program embodies a flaw, when in fact it does not.